COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	the proof COPY:
C00018 ENDMK
C⊗;
the proof COPY:

(DECL (COPY) |GROUND→GROUND| CONSTANT)

(AXIOM |∀U.COPY(U)=IF NULL(U) THEN NNIL ELSE CONS(CAR(U),COPY(CDR(U)))|)
2. ∀U.COPY(U)=IF NULL(U) THEN NNIL ELSE CONS(CAR(U),COPY(CDR(U)))
   ctxt: (1 LISP#1 LISP#5 LISP#6 LISP#7 LISP#8)   deps: NIL

(∀E PHI |λV.COPY(V)=V| LISP#17 LISP#12)
3. COPY(NNIL)=NNIL∧(∀X U.COPY(U)=U⊃COPY(CONS(X,U))=CONS(X,U))⊃(∀U.COPY(U)=U)
   ctxt: (1 LISP#1 LISP#2 LISP#5 LISP#6)   deps: NIL

(DECSIMP |∀X U.COPY(CONS(X,U))=CONS(X,COPY(U))| SRIGHT NIL NIL (LISP#12) 2
 LISP#14 LISP#15 LISP#16)
4. ∀X U.COPY(CONS(X,U))=CONS(X,COPY(U))
   ctxt: (1 LISP#1 LISP#2 LISP#6)   deps: NIL

(DECSIMP |∀U.COPY(U)=U| SRIGHT (3) NIL (LISP#12) 2 LISP#13 4)
5. ∀U.COPY(U)=U
   ctxt: (1 LISP#1)   deps: NIL